<html>
<head><meta charset="utf-8"><title>the guarantees of const - half-measures · t-lang · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/index.html">t-lang</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html">the guarantees of const - half-measures</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="247317594"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/the%20guarantees%20of%20const%20-%20half-measures/near/247317594" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html#247317594">(Jul 27 2021 at 10:48)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> I remember that "if the const fn evaluates successfully at compile-time for some given arguments, it must evaluate the same at runtime for the same arguments" was a possible rule stated previously. Making it UB for that to be violated was "unprovable UB", right? That would break with all other UB we have, or am I misremembering?</p>



<a name="247318963"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/the%20guarantees%20of%20const%20-%20half-measures/near/247318963" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html#247318963">(Jul 27 2021 at 11:05)</a>:</h4>
<p>if we <em>dont</em> have a "const select" mechanism (different code for CTFE and runtime), then a similar property is guaranteed: "if the const fn evaluates successfully at compile-time for some arguments, then it must <em>be possible</em> for this function to evaluate to the same result at runtime". This takes into account non-determinism, i.e. the runtime function might have multiple different results and compiletime picked one.</p>



<a name="247318994"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/the%20guarantees%20of%20const%20-%20half-measures/near/247318994" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html#247318994">(Jul 27 2021 at 11:05)</a>:</h4>
<p>that is just stating that the CTFE engine is correctly evaluating code according to the same semantics that we use at runtime</p>



<a name="247319161"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/the%20guarantees%20of%20const%20-%20half-measures/near/247319161" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html#247319161">(Jul 27 2021 at 11:07)</a>:</h4>
<p>with a "const select" mechanism, of course we cannot guarantee this any more. we could say it is UB to violate that property but I think UB is the wrong tool for this job... the condition is just too complicated for UB to be a good solution IMO -- this is "untestable UB". (it is not "unprovable", proofs can do [almost] anything.)</p>



<a name="247319194"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/the%20guarantees%20of%20const%20-%20half-measures/near/247319194" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html#247319194">(Jul 27 2021 at 11:07)</a>:</h4>
<p>but we can still make this condition part of what it means for a public <code>const fn</code> to be <em>sound</em></p>



<a name="247319204"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/the%20guarantees%20of%20const%20-%20half-measures/near/247319204" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html#247319204">(Jul 27 2021 at 11:07)</a>:</h4>
<p>soundness is not testable already anyway^^</p>



<a name="247319677"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/the%20guarantees%20of%20const%20-%20half-measures/near/247319677" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Connor Horman <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html#247319677">(Jul 27 2021 at 11:13)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures/near/247319161">said</a>:</p>
<blockquote>
<p>with a "const select" mechanism, of course we cannot guarantee this any more. we could say it is UB to violate that property but I think UB is the wrong tool for this job... the condition is just too complicated for UB to be a good solution IMO -- this is "untestable UB". (it is not "unprovable", proofs can do [almost] anything.)</p>
</blockquote>
<p>Well, it could be tested by trial evaluation. Miri could, when calling a const function that uses <code>const_select</code>, evaluate both branches, the <code>const</code> branch in CTFE mode and the non-<code>const</code> branch not.  If the <code>const</code> branch resolves, but the runtime branch explicitly diverges (exits, aborts, or uncaught panic), then the function has undefined behaviour and miri could signal an error.  I do not know how viable this is, but this would be a way to detect it.</p>



<a name="247327633"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/the%20guarantees%20of%20const%20-%20half-measures/near/247327633" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html#247327633">(Jul 27 2021 at 12:44)</a>:</h4>
<p>bu what if both return, but with different results? due to non-determinism that could still be correct...</p>



<a name="247327671"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/the%20guarantees%20of%20const%20-%20half-measures/near/247327671" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html#247327671">(Jul 27 2021 at 12:45)</a>:</h4>
<p>also this breaks down for higher-order functions, where equality is no longer decidable</p>



<a name="247327714"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/the%20guarantees%20of%20const%20-%20half-measures/near/247327714" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html#247327714">(Jul 27 2021 at 12:45)</a>:</h4>
<p>like calling a <code>const fn</code> that returns a <code>impl FnOnce</code></p>



<a name="247328103"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/the%20guarantees%20of%20const%20-%20half-measures/near/247328103" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Connor Horman <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html#247328103">(Jul 27 2021 at 12:49)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures/near/247327633">said</a>:</p>
<blockquote>
<p>bu what if both return, but with different results? due to non-determinism that could still be correct...</p>
</blockquote>
<p>If both return then the runtime version is the correct version according to the behaviour of <br>
(the fictional) <code>const_select</code>. I don't think that having different results itself should be UB (otherwise, you can't optimize float functions, as I mentioned). This only provides a method for checking the property of if the <code>const</code> path does not error or have undefined behaviour, then the non-<code>const</code> path will converge (and also notably does not check if the non-<code>const</code> path enters an infinite loop, which cannot be detected).</p>



<a name="247329998"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/the%20guarantees%20of%20const%20-%20half-measures/near/247329998" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html#247329998">(Jul 27 2021 at 13:05)</a>:</h4>
<p>if both are allowed to return different results, then I dont see how this helps at all wrt the condition we are talking about</p>



<a name="247330041"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/the%20guarantees%20of%20const%20-%20half-measures/near/247330041" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/the.20guarantees.20of.20const.20-.20half-measures.html#247330041">(Jul 27 2021 at 13:05)</a>:</h4>
<p>which is "if the const fn evaluates successfully at compile-time for some arguments, then it must be possible for this function to evaluate to the same result at runtime"</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>